(set-logic QF_ABV)
(set-info :source |
Ivan Jager <aij+nospam@andrew.cmu.edu>

|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unknown)
(declare-fun mem_35_703 () (Array (_ BitVec 32) (_ BitVec 8)))
(declare-fun R_EDX_8_86 () (_ BitVec 32))
(declare-fun R_EBX_6_81 () (_ BitVec 32))
(declare-fun R_ECX_7_79 () (_ BitVec 32))
(declare-fun R_ESI_2_75 () (_ BitVec 32))
(declare-fun R_EAX_5_64 () (_ BitVec 32))
(declare-fun R_EBP_0_60 () (_ BitVec 32))
(declare-fun R_ESP_1_58 () (_ BitVec 32))
(assert (let ((?v_0 (bvsub (bvsub R_ESP_1_58 (_ bv4 32)) (_ bv4 32)))) (let ((?v_3 (bvsub ?v_0 (_ bv4 32)))) (let ((?v_5 (bvadd (bvadd (bvadd ?v_3 (_ bv4 32)) (_ bv4 32)) (_ bv4 32))) (?v_1 (bvsub ?v_3 (_ bv4 32)))) (let ((?v_2 (bvsub (bvsub ?v_1 (_ bv4 32)) (_ bv4 32)))) (let ((?v_4 (store (store (store (store (store (store (store (store (store (store (store (store mem_35_703 (bvadd ?v_0 (_ bv3 32)) ((_ extract 7 0) (bvlshr R_EBP_0_60 (_ bv24 32)))) (bvadd ?v_0 (_ bv2 32)) ((_ extract 7 0) (bvlshr R_EBP_0_60 (_ bv16 32)))) (bvadd ?v_0 (_ bv1 32)) ((_ extract 7 0) (bvlshr R_EBP_0_60 (_ bv8 32)))) (bvadd ?v_0 (_ bv0 32)) ((_ extract 7 0) R_EBP_0_60)) (bvadd ?v_1 (_ bv3 32)) ((_ extract 7 0) (bvlshr R_ESI_2_75 (_ bv24 32)))) (bvadd ?v_1 (_ bv2 32)) ((_ extract 7 0) (bvlshr R_ESI_2_75 (_ bv16 32)))) (bvadd ?v_1 (_ bv1 32)) ((_ extract 7 0) (bvlshr R_ESI_2_75 (_ bv8 32)))) (bvadd ?v_1 (_ bv0 32)) ((_ extract 7 0) R_ESI_2_75)) (bvadd ?v_2 (_ bv3 32)) ((_ extract 7 0) (bvlshr R_EBX_6_81 (_ bv24 32)))) (bvadd ?v_2 (_ bv2 32)) ((_ extract 7 0) (bvlshr R_EBX_6_81 (_ bv16 32)))) (bvadd ?v_2 (_ bv1 32)) ((_ extract 7 0) (bvlshr R_EBX_6_81 (_ bv8 32)))) (bvadd ?v_2 (_ bv0 32)) ((_ extract 7 0) R_EBX_6_81)))) (let ((?v_21 (ite (not (= (bvor (bvor (bvor (concat (_ bv0 24) (select mem_35_703 (bvadd R_ESP_1_58 (_ bv0 32)))) (bvshl (concat (_ bv0 24) (select mem_35_703 (bvadd R_ESP_1_58 (_ bv1 32)))) (_ bv8 32))) (bvshl (concat (_ bv0 24) (select mem_35_703 (bvadd R_ESP_1_58 (_ bv2 32)))) (_ bv16 32))) (bvshl (concat (_ bv0 24) (select mem_35_703 (bvadd R_ESP_1_58 (_ bv3 32)))) (_ bv24 32))) (bvor (bvor (bvor (concat (_ bv0 24) (select ?v_4 (bvadd ?v_5 (_ bv0 32)))) (bvshl (concat (_ bv0 24) (select ?v_4 (bvadd ?v_5 (_ bv1 32)))) (_ bv8 32))) (bvshl (concat (_ bv0 24) (select ?v_4 (bvadd ?v_5 (_ bv2 32)))) (_ bv16 32))) (bvshl (concat (_ bv0 24) (select ?v_4 (bvadd ?v_5 (_ bv3 32)))) (_ bv24 32))))) (_ bv1 1) (_ bv0 1))) (?v_27 (bvand R_EDX_8_86 (_ bv4294967040 32))) (?v_16 (bvsub R_ECX_7_79 (_ bv9 32)))) (let ((?v_50 (bvor ?v_27 (concat (_ bv0 24) (concat (_ bv0 7) ((_ extract 0 0) (concat (_ bv0 31) (ite (= ?v_16 (_ bv0 32)) (_ bv1 1) (_ bv0 1)))))))) (?v_6 (bvand R_EDX_8_86 (_ bv61440 32)))) (let ((?v_20 (bvsub ?v_6 (_ bv32768 32)))) (let ((?v_19 (bvor (bvand ?v_6 (_ bv4294967040 32)) (concat (_ bv0 24) (concat (_ bv0 7) ((_ extract 0 0) (concat (_ bv0 31) (ite (= ?v_20 (_ bv0 32)) (_ bv1 1) (_ bv0 1)))))))) (?v_17 (bvsub R_ECX_7_79 (_ bv3 32)))) (let ((?v_51 (concat (_ bv0 24) (concat (_ bv0 7) ((_ extract 0 0) (concat (_ bv0 31) (ite (= ?v_17 (_ bv0 32)) (_ bv1 1) (_ bv0 1)))))))) (let ((?v_15 (bvor ?v_50 (bvor (bvand ?v_19 (_ bv4294967040 32)) ?v_51)))) (let ((?v_45 (bvand ?v_15 (_ bv4294967040 32))) (?v_12 (bvsub ?v_6 (_ bv40960 32)))) (let ((?v_28 (concat (_ bv0 24) (concat (_ bv0 7) ((_ extract 0 0) (concat (_ bv0 31) (ite (= ?v_12 (_ bv0 32)) (_ bv1 1) (_ bv0 1)))))))) (let ((?v_11 (bvor ?v_45 ?v_28))) (let ((?v_41 (bvand ?v_11 (_ bv4294967040 32))) (?v_9 (bvsub ?v_6 (_ bv4096 32)))) (let ((?v_29 (concat (_ bv0 24) (concat (_ bv0 7) ((_ extract 0 0) (concat (_ bv0 31) (ite (= ?v_9 (_ bv0 32)) (_ bv1 1) (_ bv0 1)))))))) (let ((?v_8 (bvor ?v_41 ?v_29))) (let ((?v_24 (bvand ?v_8 (_ bv4294967040 32))) (?v_7 (bvsub ?v_6 (_ bv49152 32)))) (let ((?v_30 (concat (_ bv0 24) (concat (_ bv0 7) ((_ extract 0 0) (concat (_ bv0 31) (ite (= ?v_7 (_ bv0 32)) (_ bv1 1) (_ bv0 1)))))))) (let ((?v_22 ((_ extract 0 0) (concat (_ bv0 31) (ite (= (concat (_ bv0 24) ((_ extract 7 0) (bvor ?v_24 ?v_30))) (_ bv0 32)) (_ bv1 1) (_ bv0 1))))) (?v_31 (bvnot (ite (= (_ bv1 32) (bvand (_ bv1 32) (bvlshr (bvand (bvxor ?v_6 (_ bv49152 32)) (bvxor ?v_6 ?v_7)) (_ bv31 32)))) (_ bv1 1) (_ bv0 1)))) (?v_18 ((_ extract 0 0) (concat (_ bv0 31) (ite (= (concat (_ bv0 24) ((_ extract 7 0) R_EAX_5_64)) (_ bv0 32)) (_ bv1 1) (_ bv0 1)))))) (let ((?v_10 (bvnot ?v_18)) (?v_183 ((_ extract 0 0) (concat (_ bv0 31) (ite (= (concat (_ bv0 24) ((_ extract 7 0) ?v_8)) (_ bv0 32)) (_ bv1 1) (_ bv0 1))))) (?v_33 (bvnot (ite (= (_ bv1 32) (bvand (_ bv1 32) (bvlshr (bvand (bvxor ?v_6 (_ bv4096 32)) (bvxor ?v_6 ?v_9)) (_ bv31 32)))) (_ bv1 1) (_ bv0 1)))) (?v_216 ((_ extract 0 0) (concat (_ bv0 31) (ite (= (concat (_ bv0 24) ((_ extract 7 0) ?v_11)) (_ bv0 32)) (_ bv1 1) (_ bv0 1))))) (?v_35 (bvnot (ite (= (_ bv1 32) (bvand (_ bv1 32) (bvlshr (bvand (bvxor ?v_6 (_ bv40960 32)) (bvxor ?v_6 ?v_12)) (_ bv31 32)))) (_ bv1 1) (_ bv0 1)))) (?v_13 (bvor (bvor (bvor (concat (_ bv0 24) (select ?v_4 (_ bv134596172 32))) (bvshl (concat (_ bv0 24) (select ?v_4 (_ bv134596173 32))) (_ bv8 32))) (bvshl (concat (_ bv0 24) (select ?v_4 (_ bv134596174 32))) (_ bv16 32))) (bvshl (concat (_ bv0 24) (select ?v_4 (_ bv134596175 32))) (_ bv24 32))))) (let ((?v_14 (bvsub ?v_13 (_ bv1 32)))) (let ((?v_230 ((_ extract 0 0) (concat (_ bv0 31) (ite (= ?v_14 (_ bv0 32)) (_ bv1 1) (_ bv0 1)))))) (let ((?v_36 (bvnot ?v_230)) (?v_37 (bvnot (ite (= (_ bv1 32) (bvand (_ bv1 32) (bvlshr (bvand (bvxor ?v_13 (_ bv1 32)) (bvxor ?v_13 ?v_14)) (_ bv31 32)))) (_ bv1 1) (_ bv0 1)))) (?v_234 ((_ extract 0 0) (concat (_ bv0 31) (ite (= (concat (_ bv0 24) ((_ extract 7 0) ?v_15)) (_ bv0 32)) (_ bv1 1) (_ bv0 1))))) (?v_55 (bvnot (ite (= (_ bv1 32) (bvand (_ bv1 32) (bvlshr (bvand (bvxor R_ECX_7_79 (_ bv9 32)) (bvxor R_ECX_7_79 ?v_16)) (_ bv31 32)))) (_ bv1 1) (_ bv0 1)))) (?v_56 (bvnot (ite (= (_ bv1 32) (bvand (_ bv1 32) (bvlshr (bvand (bvxor R_ECX_7_79 (_ bv3 32)) (bvxor R_ECX_7_79 ?v_17)) (_ bv31 32)))) (_ bv1 1) (_ bv0 1)))) (?v_241 ((_ extract 0 0) (concat (_ bv0 31) (ite (= (concat (_ bv0 24) ((_ extract 7 0) ?v_19)) (_ bv0 32)) (_ bv1 1) (_ bv0 1))))) (?v_242 (bvand (bvnot (ite (= (_ bv1 32) (bvand (_ bv1 32) (bvlshr (bvand (bvxor ?v_6 (_ bv32768 32)) (bvxor ?v_6 ?v_20)) (_ bv31 32)))) (_ bv1 1) (_ bv0 1))) (bvand ?v_10 (_ bv1 1))))) (let ((?v_40 (bvand ?v_241 ?v_242))) (let ((?v_235 (bvand ?v_55 (bvand ?v_56 (bvand ?v_18 ?v_40))))) (let ((?v_231 (bvand ?v_37 (bvand ?v_234 ?v_235)))) (let ((?v_49 (bvand ?v_36 ?v_231))) (let ((?v_217 (bvand ?v_35 (bvand ?v_10 ?v_49)))) (let ((?v_44 (bvand ?v_216 ?v_217))) (let ((?v_184 (bvand ?v_33 (bvand ?v_10 ?v_44)))) (let ((?v_26 (bvand ?v_183 ?v_184))) (let ((?v_23 (bvand ?v_31 (bvand ?v_10 ?v_26))) (?v_25 (bvsub R_ECX_7_79 (_ bv7 32)))) (let ((?v_68 (concat (_ bv0 24) (concat (_ bv0 7) ((_ extract 0 0) (concat (_ bv0 31) (ite (= ?v_25 (_ bv0 32)) (_ bv1 1) (_ bv0 1)))))))) (let ((?v_59 ((_ extract 0 0) (concat (_ bv0 31) (ite (= (concat (_ bv0 24) ((_ extract 7 0) (bvor ?v_24 ?v_68))) (_ bv0 32)) (_ bv1 1) (_ bv0 1))))) (?v_69 (bvnot (ite (= (_ bv1 32) (bvand (_ bv1 32) (bvlshr (bvand (bvxor R_ECX_7_79 (_ bv7 32)) (bvxor R_ECX_7_79 ?v_25)) (_ bv31 32)))) (_ bv1 1) (_ bv0 1))))) (let ((?v_60 (bvand ?v_69 (bvand ?v_18 ?v_26))) (?v_39 (bvsub ?v_6 (_ bv16384 32)))) (let ((?v_38 (bvor ?v_27 (concat (_ bv0 24) (concat (_ bv0 7) ((_ extract 0 0) (concat (_ bv0 31) (ite (= ?v_39 (_ bv0 32)) (_ bv1 1) (_ bv0 1))))))))) (let ((?v_84 (bvand ?v_38 (_ bv4294967040 32)))) (let ((?v_34 (bvor ?v_84 ?v_28))) (let ((?v_79 (bvand ?v_34 (_ bv4294967040 32)))) (let ((?v_32 (bvor ?v_79 ?v_29))) (let ((?v_67 (bvand ?v_32 (_ bv4294967040 32)))) (let ((?v_61 ((_ extract 0 0) (concat (_ bv0 31) (ite (= (concat (_ bv0 24) ((_ extract 7 0) (bvor ?v_67 ?v_30))) (_ bv0 32)) (_ bv1 1) (_ bv0 1))))) (?v_93 ((_ extract 0 0) (concat (_ bv0 31) (ite (= (concat (_ bv0 24) ((_ extract 7 0) ?v_32)) (_ bv0 32)) (_ bv1 1) (_ bv0 1))))) (?v_94 ((_ extract 0 0) (concat (_ bv0 31) (ite (= (concat (_ bv0 24) ((_ extract 7 0) ?v_34)) (_ bv0 32)) (_ bv1 1) (_ bv0 1))))) (?v_95 ((_ extract 0 0) (concat (_ bv0 31) (ite (= (concat (_ bv0 24) ((_ extract 7 0) ?v_38)) (_ bv0 32)) (_ bv1 1) (_ bv0 1))))) (?v_96 (bvnot (ite (= (_ bv1 32) (bvand (_ bv1 32) (bvlshr (bvand (bvxor ?v_6 (_ bv16384 32)) (bvxor ?v_6 ?v_39)) (_ bv31 32)))) (_ bv1 1) (_ bv0 1))))) (let ((?v_237 (bvand ?v_96 (bvand ?v_10 ?v_40)))) (let ((?v_232 (bvand ?v_37 (bvand ?v_95 ?v_237)))) (let ((?v_89 (bvand ?v_36 ?v_232))) (let ((?v_218 (bvand ?v_35 (bvand ?v_10 ?v_89)))) (let ((?v_83 (bvand ?v_94 ?v_218))) (let ((?v_190 (bvand ?v_33 (bvand ?v_10 ?v_83)))) (let ((?v_70 (bvand ?v_93 ?v_190))) (let ((?v_62 (bvand ?v_31 (bvand ?v_10 ?v_70))) (?v_43 (bvsub R_ECX_7_79 (_ bv1 32)))) (let ((?v_80 (concat (_ bv0 24) (concat (_ bv0 7) ((_ extract 0 0) (concat (_ bv0 31) (ite (= ?v_43 (_ bv0 32)) (_ bv1 1) (_ bv0 1)))))))) (let ((?v_42 (bvor ?v_41 ?v_80))) (let ((?v_71 (bvand ?v_42 (_ bv4294967040 32)))) (let ((?v_63 ((_ extract 0 0) (concat (_ bv0 31) (ite (= (concat (_ bv0 24) ((_ extract 7 0) (bvor ?v_71 ?v_30))) (_ bv0 32)) (_ bv1 1) (_ bv0 1))))) (?v_191 ((_ extract 0 0) (concat (_ bv0 31) (ite (= (concat (_ bv0 24) ((_ extract 7 0) ?v_42)) (_ bv0 32)) (_ bv1 1) (_ bv0 1))))) (?v_82 (bvnot (ite (= (_ bv1 32) (bvand (_ bv1 32) (bvlshr (bvand (bvxor R_ECX_7_79 (_ bv1 32)) (bvxor R_ECX_7_79 ?v_43)) (_ bv31 32)))) (_ bv1 1) (_ bv0 1))))) (let ((?v_192 (bvand ?v_82 (bvand ?v_18 ?v_44)))) (let ((?v_72 (bvand ?v_191 ?v_192))) (let ((?v_64 (bvand ?v_31 (bvand ?v_10 ?v_72))) (?v_48 (bvsub R_ECX_7_79 (_ bv6 32)))) (let ((?v_85 (concat (_ bv0 24) (concat (_ bv0 7) ((_ extract 0 0) (concat (_ bv0 31) (ite (= ?v_48 (_ bv0 32)) (_ bv1 1) (_ bv0 1)))))))) (let ((?v_47 (bvor ?v_45 ?v_85))) (let ((?v_90 (bvand ?v_47 (_ bv4294967040 32)))) (let ((?v_46 (bvor ?v_90 ?v_29))) (let ((?v_73 (bvand ?v_46 (_ bv4294967040 32)))) (let ((?v_65 ((_ extract 0 0) (concat (_ bv0 31) (ite (= (concat (_ bv0 24) ((_ extract 7 0) (bvor ?v_73 ?v_30))) (_ bv0 32)) (_ bv1 1) (_ bv0 1))))) (?v_193 ((_ extract 0 0) (concat (_ bv0 31) (ite (= (concat (_ bv0 24) ((_ extract 7 0) ?v_46)) (_ bv0 32)) (_ bv1 1) (_ bv0 1))))) (?v_219 ((_ extract 0 0) (concat (_ bv0 31) (ite (= (concat (_ bv0 24) ((_ extract 7 0) ?v_47)) (_ bv0 32)) (_ bv1 1) (_ bv0 1))))) (?v_88 (bvnot (ite (= (_ bv1 32) (bvand (_ bv1 32) (bvlshr (bvand (bvxor R_ECX_7_79 (_ bv6 32)) (bvxor R_ECX_7_79 ?v_48)) (_ bv31 32)))) (_ bv1 1) (_ bv0 1))))) (let ((?v_220 (bvand ?v_88 (bvand ?v_18 ?v_49)))) (let ((?v_92 (bvand ?v_219 ?v_220))) (let ((?v_194 (bvand ?v_33 (bvand ?v_10 ?v_92)))) (let ((?v_74 (bvand ?v_193 ?v_194))) (let ((?v_66 (bvand ?v_31 (bvand ?v_10 ?v_74))) (?v_58 (bvsub R_ECX_7_79 (_ bv5 32)))) (let ((?v_57 (bvor (bvand R_EAX_5_64 (_ bv4294967040 32)) (concat (_ bv0 24) (concat (_ bv0 7) ((_ extract 0 0) (concat (_ bv0 31) (ite (= ?v_58 (_ bv0 32)) (_ bv1 1) (_ bv0 1))))))))) (let ((?v_54 (bvor ?v_50 (bvor (bvand ?v_57 (_ bv4294967040 32)) ?v_51)))) (let ((?v_101 (bvand ?v_54 (_ bv4294967040 32)))) (let ((?v_53 (bvor ?v_101 ?v_28))) (let ((?v_98 (bvand ?v_53 (_ bv4294967040 32)))) (let ((?v_52 (bvor ?v_98 ?v_29))) (let ((?v_77 (bvand ?v_52 (_ bv4294967040 32)))) (let ((?v_75 ((_ extract 0 0) (concat (_ bv0 31) (ite (= (concat (_ bv0 24) ((_ extract 7 0) (bvor ?v_77 ?v_30))) (_ bv0 32)) (_ bv1 1) (_ bv0 1))))) (?v_195 ((_ extract 0 0) (concat (_ bv0 31) (ite (= (concat (_ bv0 24) ((_ extract 7 0) ?v_52)) (_ bv0 32)) (_ bv1 1) (_ bv0 1))))) (?v_221 ((_ extract 0 0) (concat (_ bv0 31) (ite (= (concat (_ bv0 24) ((_ extract 7 0) ?v_53)) (_ bv0 32)) (_ bv1 1) (_ bv0 1))))) (?v_238 ((_ extract 0 0) (concat (_ bv0 31) (ite (= (concat (_ bv0 24) ((_ extract 7 0) ?v_54)) (_ bv0 32)) (_ bv1 1) (_ bv0 1))))) (?v_250 ((_ extract 0 0) (concat (_ bv0 31) (ite (= (concat (_ bv0 24) ((_ extract 7 0) ?v_57)) (_ bv0 32)) (_ bv1 1) (_ bv0 1))))) (?v_251 (bvand (bvnot (ite (= (_ bv1 32) (bvand (_ bv1 32) (bvlshr (bvand (bvxor R_ECX_7_79 (_ bv5 32)) (bvxor R_ECX_7_79 ?v_58)) (_ bv31 32)))) (_ bv1 1) (_ bv0 1))) (bvand ?v_18 (_ bv1 1))))) (let ((?v_97 (bvand ?v_250 ?v_251))) (let ((?v_239 (bvand ?v_55 (bvand ?v_56 (bvand ?v_18 ?v_97))))) (let ((?v_233 (bvand ?v_37 (bvand ?v_238 ?v_239)))) (let ((?v_104 (bvand ?v_36 ?v_233))) (let ((?v_222 (bvand ?v_35 (bvand ?v_10 ?v_104)))) (let ((?v_100 (bvand ?v_221 ?v_222))) (let ((?v_196 (bvand ?v_33 (bvand ?v_10 ?v_100)))) (let ((?v_78 (bvand ?v_195 ?v_196))) (let ((?v_76 (bvand ?v_31 (bvand ?v_10 ?v_78))) (?v_123 (bvnot ?v_61)) (?v_105 ((_ extract 0 0) (concat (_ bv0 31) (ite (= (concat (_ bv0 24) ((_ extract 7 0) (bvor ?v_67 ?v_68))) (_ bv0 32)) (_ bv1 1) (_ bv0 1))))) (?v_106 (bvand ?v_69 (bvand ?v_18 ?v_70))) (?v_107 ((_ extract 0 0) (concat (_ bv0 31) (ite (= (concat (_ bv0 24) ((_ extract 7 0) (bvor ?v_71 ?v_68))) (_ bv0 32)) (_ bv1 1) (_ bv0 1))))) (?v_108 (bvand ?v_69 (bvand ?v_18 ?v_72))) (?v_109 ((_ extract 0 0) (concat (_ bv0 31) (ite (= (concat (_ bv0 24) ((_ extract 7 0) (bvor ?v_73 ?v_68))) (_ bv0 32)) (_ bv1 1) (_ bv0 1))))) (?v_110 (bvand ?v_69 (bvand ?v_18 ?v_74))) (?v_111 ((_ extract 0 0) (concat (_ bv0 31) (ite (= (concat (_ bv0 24) ((_ extract 7 0) (bvor ?v_77 ?v_68))) (_ bv0 32)) (_ bv1 1) (_ bv0 1))))) (?v_112 (bvand ?v_69 (bvand ?v_18 ?v_78))) (?v_81 (bvor ?v_79 ?v_80))) (let ((?v_119 (bvand ?v_81 (_ bv4294967040 32)))) (let ((?v_113 ((_ extract 0 0) (concat (_ bv0 31) (ite (= (concat (_ bv0 24) ((_ extract 7 0) (bvor ?v_119 ?v_30))) (_ bv0 32)) (_ bv1 1) (_ bv0 1))))) (?v_139 ((_ extract 0 0) (concat (_ bv0 31) (ite (= (concat (_ bv0 24) ((_ extract 7 0) ?v_81)) (_ bv0 32)) (_ bv1 1) (_ bv0 1))))) (?v_197 (bvand ?v_82 (bvand ?v_18 ?v_83)))) (let ((?v_120 (bvand ?v_139 ?v_197))) (let ((?v_114 (bvand ?v_31 (bvand ?v_10 ?v_120))) (?v_87 (bvor ?v_84 ?v_85))) (let ((?v_136 (bvand ?v_87 (_ bv4294967040 32)))) (let ((?v_86 (bvor ?v_136 ?v_29))) (let ((?v_121 (bvand ?v_86 (_ bv4294967040 32)))) (let ((?v_115 ((_ extract 0 0) (concat (_ bv0 31) (ite (= (concat (_ bv0 24) ((_ extract 7 0) (bvor ?v_121 ?v_30))) (_ bv0 32)) (_ bv1 1) (_ bv0 1))))) (?v_141 ((_ extract 0 0) (concat (_ bv0 31) (ite (= (concat (_ bv0 24) ((_ extract 7 0) ?v_86)) (_ bv0 32)) (_ bv1 1) (_ bv0 1))))) (?v_142 ((_ extract 0 0) (concat (_ bv0 31) (ite (= (concat (_ bv0 24) ((_ extract 7 0) ?v_87)) (_ bv0 32)) (_ bv1 1) (_ bv0 1))))) (?v_223 (bvand ?v_88 (bvand ?v_18 ?v_89)))) (let ((?v_138 (bvand ?v_142 ?v_223))) (let ((?v_198 (bvand ?v_33 (bvand ?v_10 ?v_138)))) (let ((?v_122 (bvand ?v_141 ?v_198))) (let ((?v_116 (bvand ?v_31 (bvand ?v_10 ?v_122))) (?v_91 (bvor ?v_90 ?v_80))) (let ((?v_125 (bvand ?v_91 (_ bv4294967040 32)))) (let ((?v_117 ((_ extract 0 0) (concat (_ bv0 31) (ite (= (concat (_ bv0 24) ((_ extract 7 0) (bvor ?v_125 ?v_30))) (_ bv0 32)) (_ bv1 1) (_ bv0 1))))) (?v_199 ((_ extract 0 0) (concat (_ bv0 31) (ite (= (concat (_ bv0 24) ((_ extract 7 0) ?v_91)) (_ bv0 32)) (_ bv1 1) (_ bv0 1))))) (?v_200 (bvand ?v_82 (bvand ?v_18 ?v_92)))) (let ((?v_126 (bvand ?v_199 ?v_200))) (let ((?v_118 (bvand ?v_31 (bvand ?v_10 ?v_126))) (?v_246 (bvand ?v_96 (bvand ?v_10 ?v_97)))) (let ((?v_236 (bvand ?v_37 (bvand ?v_95 ?v_246)))) (let ((?v_143 (bvand ?v_36 ?v_236))) (let ((?v_225 (bvand ?v_35 (bvand ?v_10 ?v_143)))) (let ((?v_140 (bvand ?v_94 ?v_225))) (let ((?v_202 (bvand ?v_33 (bvand ?v_10 ?v_140)))) (let ((?v_131 (bvand ?v_93 ?v_202))) (let ((?v_124 (bvand ?v_31 (bvand ?v_10 ?v_131))) (?v_99 (bvor ?v_98 ?v_80))) (let ((?v_132 (bvand ?v_99 (_ bv4294967040 32)))) (let ((?v_127 ((_ extract 0 0) (concat (_ bv0 31) (ite (= (concat (_ bv0 24) ((_ extract 7 0) (bvor ?v_132 ?v_30))) (_ bv0 32)) (_ bv1 1) (_ bv0 1))))) (?v_203 ((_ extract 0 0) (concat (_ bv0 31) (ite (= (concat (_ bv0 24) ((_ extract 7 0) ?v_99)) (_ bv0 32)) (_ bv1 1) (_ bv0 1))))) (?v_204 (bvand ?v_82 (bvand ?v_18 ?v_100)))) (let ((?v_133 (bvand ?v_203 ?v_204))) (let ((?v_128 (bvand ?v_31 (bvand ?v_10 ?v_133))) (?v_103 (bvor ?v_101 ?v_85))) (let ((?v_144 (bvand ?v_103 (_ bv4294967040 32)))) (let ((?v_102 (bvor ?v_144 ?v_29))) (let ((?v_134 (bvand ?v_102 (_ bv4294967040 32)))) (let ((?v_129 ((_ extract 0 0) (concat (_ bv0 31) (ite (= (concat (_ bv0 24) ((_ extract 7 0) (bvor ?v_134 ?v_30))) (_ bv0 32)) (_ bv1 1) (_ bv0 1))))) (?v_205 ((_ extract 0 0) (concat (_ bv0 31) (ite (= (concat (_ bv0 24) ((_ extract 7 0) ?v_102)) (_ bv0 32)) (_ bv1 1) (_ bv0 1))))) (?v_226 ((_ extract 0 0) (concat (_ bv0 31) (ite (= (concat (_ bv0 24) ((_ extract 7 0) ?v_103)) (_ bv0 32)) (_ bv1 1) (_ bv0 1))))) (?v_227 (bvand ?v_88 (bvand ?v_18 ?v_104)))) (let ((?v_146 (bvand ?v_226 ?v_227))) (let ((?v_206 (bvand ?v_33 (bvand ?v_10 ?v_146)))) (let ((?v_135 (bvand ?v_205 ?v_206))) (let ((?v_130 (bvand ?v_31 (bvand ?v_10 ?v_135))) (?v_153 (bvnot ?v_105)) (?v_163 (bvnot ?v_113)) (?v_165 (bvnot ?v_115)) (?v_147 ((_ extract 0 0) (concat (_ bv0 31) (ite (= (concat (_ bv0 24) ((_ extract 7 0) (bvor ?v_119 ?v_68))) (_ bv0 32)) (_ bv1 1) (_ bv0 1))))) (?v_148 (bvand ?v_69 (bvand ?v_18 ?v_120))) (?v_149 ((_ extract 0 0) (concat (_ bv0 31) (ite (= (concat (_ bv0 24) ((_ extract 7 0) (bvor ?v_121 ?v_68))) (_ bv0 32)) (_ bv1 1) (_ bv0 1))))) (?v_150 (bvand ?v_69 (bvand ?v_18 ?v_122))) (?v_151 ((_ extract 0 0) (concat (_ bv0 31) (ite (= (concat (_ bv0 24) ((_ extract 7 0) (bvor ?v_125 ?v_68))) (_ bv0 32)) (_ bv1 1) (_ bv0 1))))) (?v_152 (bvand ?v_69 (bvand ?v_18 ?v_126))) (?v_154 (bvand ?v_69 (bvand ?v_18 ?v_131))) (?v_155 ((_ extract 0 0) (concat (_ bv0 31) (ite (= (concat (_ bv0 24) ((_ extract 7 0) (bvor ?v_132 ?v_68))) (_ bv0 32)) (_ bv1 1) (_ bv0 1))))) (?v_156 (bvand ?v_69 (bvand ?v_18 ?v_133))) (?v_157 ((_ extract 0 0) (concat (_ bv0 31) (ite (= (concat (_ bv0 24) ((_ extract 7 0) (bvor ?v_134 ?v_68))) (_ bv0 32)) (_ bv1 1) (_ bv0 1))))) (?v_158 (bvand ?v_69 (bvand ?v_18 ?v_135))) (?v_137 (bvor ?v_136 ?v_80))) (let ((?v_161 (bvand ?v_137 (_ bv4294967040 32)))) (let ((?v_159 ((_ extract 0 0) (concat (_ bv0 31) (ite (= (concat (_ bv0 24) ((_ extract 7 0) (bvor ?v_161 ?v_30))) (_ bv0 32)) (_ bv1 1) (_ bv0 1))))) (?v_173 ((_ extract 0 0) (concat (_ bv0 31) (ite (= (concat (_ bv0 24) ((_ extract 7 0) ?v_137)) (_ bv0 32)) (_ bv1 1) (_ bv0 1))))) (?v_207 (bvand ?v_82 (bvand ?v_18 ?v_138)))) (let ((?v_162 (bvand ?v_173 ?v_207))) (let ((?v_160 (bvand ?v_31 (bvand ?v_10 ?v_162))) (?v_209 (bvand ?v_82 (bvand ?v_18 ?v_140)))) (let ((?v_169 (bvand ?v_139 ?v_209))) (let ((?v_164 (bvand ?v_31 (bvand ?v_10 ?v_169))) (?v_229 (bvand ?v_88 (bvand ?v_18 ?v_143)))) (let ((?v_174 (bvand ?v_142 ?v_229))) (let ((?v_211 (bvand ?v_33 (bvand ?v_10 ?v_174)))) (let ((?v_170 (bvand ?v_141 ?v_211))) (let ((?v_166 (bvand ?v_31 (bvand ?v_10 ?v_170))) (?v_145 (bvor ?v_144 ?v_80))) (let ((?v_171 (bvand ?v_145 (_ bv4294967040 32)))) (let ((?v_167 ((_ extract 0 0) (concat (_ bv0 31) (ite (= (concat (_ bv0 24) ((_ extract 7 0) (bvor ?v_171 ?v_30))) (_ bv0 32)) (_ bv1 1) (_ bv0 1))))) (?v_212 ((_ extract 0 0) (concat (_ bv0 31) (ite (= (concat (_ bv0 24) ((_ extract 7 0) ?v_145)) (_ bv0 32)) (_ bv1 1) (_ bv0 1))))) (?v_213 (bvand ?v_82 (bvand ?v_18 ?v_146)))) (let ((?v_172 (bvand ?v_212 ?v_213))) (let ((?v_168 (bvand ?v_31 (bvand ?v_10 ?v_172))) (?v_177 (bvnot ?v_147)) (?v_179 (bvnot ?v_149)) (?v_185 (bvnot ?v_159)) (?v_175 ((_ extract 0 0) (concat (_ bv0 31) (ite (= (concat (_ bv0 24) ((_ extract 7 0) (bvor ?v_161 ?v_68))) (_ bv0 32)) (_ bv1 1) (_ bv0 1))))) (?v_176 (bvand ?v_69 (bvand ?v_18 ?v_162))) (?v_178 (bvand ?v_69 (bvand ?v_18 ?v_169))) (?v_180 (bvand ?v_69 (bvand ?v_18 ?v_170))) (?v_181 ((_ extract 0 0) (concat (_ bv0 31) (ite (= (concat (_ bv0 24) ((_ extract 7 0) (bvor ?v_171 ?v_68))) (_ bv0 32)) (_ bv1 1) (_ bv0 1))))) (?v_182 (bvand ?v_69 (bvand ?v_18 ?v_172))) (?v_215 (bvand ?v_82 (bvand ?v_18 ?v_174)))) (let ((?v_187 (bvand ?v_173 ?v_215))) (let ((?v_186 (bvand ?v_31 (bvand ?v_10 ?v_187))) (?v_188 (bvnot ?v_175)) (?v_189 (bvand ?v_69 (bvand ?v_18 ?v_187))) (?v_201 (bvnot ?v_93)) (?v_208 (bvnot ?v_139)) (?v_210 (bvnot ?v_141)) (?v_214 (bvnot ?v_173)) (?v_224 (bvnot ?v_94)) (?v_228 (bvnot ?v_142)) (?v_245 (bvnot ?v_95)) (?v_243 ((_ extract 0 0) (concat (_ bv0 31) (ite (= (bvand R_EDX_8_86 (_ bv73 32)) (_ bv0 32)) (_ bv1 1) (_ bv0 1))))) (?v_240 (bvsub ?v_13 (_ bv3 32)))) (let ((?v_247 ((_ extract 0 0) (concat (_ bv0 31) (ite (= ?v_240 (_ bv0 32)) (_ bv1 1) (_ bv0 1))))) (?v_249 (bvnot (ite (= (_ bv1 32) (bvand (_ bv1 32) (bvlshr (bvand (bvxor ?v_13 (_ bv3 32)) (bvxor ?v_13 ?v_240)) (_ bv31 32)))) (_ bv1 1) (_ bv0 1)))) (?v_256 (bvand (bvnot ?v_241) ?v_242))) (let ((?v_248 (bvand ?v_249 (bvand ?v_10 ?v_256)))) (let ((?v_244 (bvand ?v_247 ?v_248)) (?v_252 (bvnot ?v_243)) (?v_254 (bvnot ?v_247)) (?v_257 (bvand (bvnot ?v_250) ?v_251))) (let ((?v_255 (bvand ?v_249 (bvand ?v_10 ?v_257)))) (let ((?v_253 (bvand ?v_247 ?v_255))) (= (_ bv1 1) (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvor (bvand ?v_21 (bvand ?v_22 ?v_23)) (bvand ?v_21 (bvand (bvnot ?v_22) ?v_23))) (bvand ?v_21 (bvand ?v_59 ?v_60))) (bvand ?v_21 (bvand ?v_61 ?v_62))) (bvand ?v_21 (bvand ?v_63 ?v_64))) (bvand ?v_21 (bvand ?v_65 ?v_66))) (bvand ?v_21 (bvand ?v_75 ?v_76))) (bvand ?v_21 (bvand (bvnot ?v_59) ?v_60))) (bvand ?v_21 (bvand ?v_123 ?v_62))) (bvand ?v_21 (bvand (bvnot ?v_63) ?v_64))) (bvand ?v_21 (bvand (bvnot ?v_65) ?v_66))) (bvand ?v_21 (bvand ?v_105 ?v_106))) (bvand ?v_21 (bvand ?v_107 ?v_108))) (bvand ?v_21 (bvand ?v_109 ?v_110))) (bvand ?v_21 (bvand (bvnot ?v_75) ?v_76))) (bvand ?v_21 (bvand ?v_111 ?v_112))) (bvand ?v_21 (bvand ?v_113 ?v_114))) (bvand ?v_21 (bvand ?v_115 ?v_116))) (bvand ?v_21 (bvand ?v_117 ?v_118))) (bvand ?v_21 (bvand ?v_61 ?v_124))) (bvand ?v_21 (bvand ?v_127 ?v_128))) (bvand ?v_21 (bvand ?v_129 ?v_130))) (bvand ?v_21 (bvand ?v_153 ?v_106))) (bvand ?v_21 (bvand (bvnot ?v_107) ?v_108))) (bvand ?v_21 (bvand (bvnot ?v_109) ?v_110))) (bvand ?v_21 (bvand (bvnot ?v_111) ?v_112))) (bvand ?v_21 (bvand ?v_163 ?v_114))) (bvand ?v_21 (bvand ?v_165 ?v_116))) (bvand ?v_21 (bvand (bvnot ?v_117) ?v_118))) (bvand ?v_21 (bvand ?v_147 ?v_148))) (bvand ?v_21 (bvand ?v_149 ?v_150))) (bvand ?v_21 (bvand ?v_123 ?v_124))) (bvand ?v_21 (bvand ?v_151 ?v_152))) (bvand ?v_21 (bvand (bvnot ?v_127) ?v_128))) (bvand ?v_21 (bvand (bvnot ?v_129) ?v_130))) (bvand ?v_21 (bvand ?v_105 ?v_154))) (bvand ?v_21 (bvand ?v_155 ?v_156))) (bvand ?v_21 (bvand ?v_157 ?v_158))) (bvand ?v_21 (bvand ?v_159 ?v_160))) (bvand ?v_21 (bvand ?v_113 ?v_164))) (bvand ?v_21 (bvand ?v_115 ?v_166))) (bvand ?v_21 (bvand ?v_167 ?v_168))) (bvand ?v_21 (bvand ?v_177 ?v_148))) (bvand ?v_21 (bvand ?v_179 ?v_150))) (bvand ?v_21 (bvand (bvnot ?v_151) ?v_152))) (bvand ?v_21 (bvand ?v_153 ?v_154))) (bvand ?v_21 (bvand (bvnot ?v_155) ?v_156))) (bvand ?v_21 (bvand (bvnot ?v_157) ?v_158))) (bvand ?v_21 (bvand ?v_185 ?v_160))) (bvand ?v_21 (bvand ?v_175 ?v_176))) (bvand ?v_21 (bvand ?v_163 ?v_164))) (bvand ?v_21 (bvand ?v_165 ?v_166))) (bvand ?v_21 (bvand (bvnot ?v_167) ?v_168))) (bvand ?v_21 (bvand ?v_147 ?v_178))) (bvand ?v_21 (bvand ?v_149 ?v_180))) (bvand ?v_21 (bvand ?v_181 ?v_182))) (bvand ?v_21 (bvand ?v_159 ?v_186))) (bvand ?v_21 (bvand ?v_188 ?v_176))) (bvand ?v_21 (bvand ?v_177 ?v_178))) (bvand ?v_21 (bvand ?v_179 ?v_180))) (bvand ?v_21 (bvand (bvnot ?v_181) ?v_182))) (bvand ?v_21 (bvand (bvnot ?v_183) ?v_184))) (bvand ?v_21 (bvand ?v_185 ?v_186))) (bvand ?v_21 (bvand ?v_175 ?v_189))) (bvand ?v_21 (bvand ?v_188 ?v_189))) (bvand ?v_21 (bvand ?v_201 ?v_190))) (bvand ?v_21 (bvand (bvnot ?v_191) ?v_192))) (bvand ?v_21 (bvand (bvnot ?v_193) ?v_194))) (bvand ?v_21 (bvand (bvnot ?v_195) ?v_196))) (bvand ?v_21 (bvand ?v_208 ?v_197))) (bvand ?v_21 (bvand ?v_210 ?v_198))) (bvand ?v_21 (bvand (bvnot ?v_199) ?v_200))) (bvand ?v_21 (bvand ?v_201 ?v_202))) (bvand ?v_21 (bvand (bvnot ?v_203) ?v_204))) (bvand ?v_21 (bvand (bvnot ?v_205) ?v_206))) (bvand ?v_21 (bvand ?v_214 ?v_207))) (bvand ?v_21 (bvand ?v_208 ?v_209))) (bvand ?v_21 (bvand ?v_210 ?v_211))) (bvand ?v_21 (bvand (bvnot ?v_212) ?v_213))) (bvand ?v_21 (bvand ?v_214 ?v_215))) (bvand ?v_21 (bvand (bvnot ?v_216) ?v_217))) (bvand ?v_21 (bvand ?v_224 ?v_218))) (bvand ?v_21 (bvand (bvnot ?v_219) ?v_220))) (bvand ?v_21 (bvand (bvnot ?v_221) ?v_222))) (bvand ?v_21 (bvand ?v_228 ?v_223))) (bvand ?v_21 (bvand ?v_224 ?v_225))) (bvand ?v_21 (bvand (bvnot ?v_226) ?v_227))) (bvand ?v_21 (bvand ?v_228 ?v_229))) (bvand ?v_21 (bvand ?v_230 ?v_231))) (bvand ?v_21 (bvand ?v_230 ?v_232))) (bvand ?v_21 (bvand ?v_230 ?v_233))) (bvand ?v_21 (bvand (bvnot ?v_234) ?v_235))) (bvand ?v_21 (bvand ?v_230 ?v_236))) (bvand ?v_21 (bvand ?v_245 ?v_237))) (bvand ?v_21 (bvand (bvnot ?v_238) ?v_239))) (bvand ?v_21 (bvand ?v_243 ?v_244))) (bvand ?v_21 (bvand ?v_252 ?v_244))) (bvand ?v_21 (bvand ?v_245 ?v_246))) (bvand ?v_21 (bvand ?v_254 ?v_248))) (bvand ?v_21 (bvand ?v_243 ?v_253))) (bvand ?v_21 (bvand ?v_252 ?v_253))) (bvand ?v_21 (bvand ?v_254 ?v_255))) (bvand ?v_21 (bvand ?v_18 ?v_256))) (bvand ?v_21 (bvand ?v_18 ?v_257)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(check-sat)
(exit)
